Лямбда кодування
НАМО ЛЯМБДАГАРБХА
Так, як ви всі знаєте, в PTS системах для кодування індуктивних типів даних прийнято використовувати лямбда числення. Всі ви знаєте про кодування Church, Parigot, Scott. Якщо хто забув, я швидко нагадаю! Але є одне особливе кодування, яке краще ніж усі ці кодування, але яке чомусь зовсім не описане в літературі, але описане було Майя Віктором (Бразилія). Його ж синтаксис Caramel використовувався для демонстрації всіх кодувань у нетипизованому лямбда-численні.
Будемо використовувати інфіксну дужкову форму запису лямбди: "(a b -> c)" означає "λ a b . c", щоб λ не дратувала очі і легше було розпізнати візерунок послідовності.
Church кодування
Сама проста. Вона зображає структуру у вигляді своїх правих фолдів. Будемо розглядати найпростіші структури даних, натуральні числа. Вони ж використовуються для чистого моделювання всесвітів тайпчекера.
0 = (f x -> x)
1 = (f x -> (f x))
2 = (f x -> (f (f x)))
3 = (f x -> (f (f (f x))))
pred = (n (g h -> (h (g succ))) (const zero) id) — O(n), погано.
foldNat = (s z nat -> (nat s z)) — Нерекурсивний, добре.
З нею є "маленька" проблема: pred такого числа або tail списку займає O(n).
Scott кодування
Дана Скотт запропонував кодувати структури не у вигляді їх правих фолдів, а у вигляді патерн-мачінг елімінаторів.
0 = (f x -> x)
1 = (f x -> (f (f x -> x)))
2 = (f x -> (f (f x -> (f (f x -> x)))))
3 = (f x -> (f (f x -> (f (f x -> (f (f x -> x)))))))
pred = (nat -> (nat (pred -> pred) _)) — O(1), добре.
foldNat = (s z nat -> (nat (pred -> (s (foldNat s z pred))) z)) — Рекурсія, погано.
Для такого кодування у нас pred натурального числа займає константний час, але для його вираження потрібна рекурсія. А ми це в Групоїд Інфініті ніяк не можемо дозволити.
Кодування Parigot
Є сумішшю Скотт і Чорч кодувань. Парігот елімінує рекурсію з фолдів.
0 = (f x -> x)
1 = (f x -> (f (f x -> (f x)) (f x -> x)))
2 = (f x -> (f (f x -> (f (f x))) (f x -> (f (f x -> (f x)) (f x -> x)))))
3 = (f x -> (f (f x -> (f (f (f x)))) (f x -> (f (f x -> (f (f x))) (f x -> (f (f x -> (f x)) (f x -> x)))))))
pred = (nat -> (nat (_ pred -> pred) _)) -- O(1), добре.
foldNat = (nat -> (nat (fold _ -> fold) _)) -- нерекурсивно, добре.
Як ви бачите Парігот начебто OK, але терми ростуть як на дріжджах, себто експоненційно. Однак, ми можемо позбутися цього!
Кодування CPS
Замість нумералів Чорча ми зберігаємо континуатори (c -> (c f x)). Опис цього кодування ви не знайдете в інтернеті в жодному пейпері.
0 = (f x -> x)
1 = (f x -> (f (c -> (c f x)) (f x -> x)))
2 = (f x -> (f (c -> (c f x)) (f x -> (f (c -> (c f x)) (f x -> x)))))
3 = (f x -> (f (c -> (c f x)) (f x -> (f (c -> (c f x)) (f x -> (f (c -> (c f x)) (f x -> x)))))))
pred = (nat -> (nat (_ pred -> pred) _)) — O(1), добре!
foldNat = (s z nat -> (nat (cont pred -> (s (cont pred))) z)) — нерекурсивна, добре!
Терми всі ростуть так як при Чорчі просто множаться на константу - розмір континуатора. Одна проблема, шо для цього кодування потрібні Self-типи Пенг-Фу і Ко, слабка форма рекурсивних типів. Але індукція і все інше виходить безкоштовно для цього кодування.
Бенчмарк CPS кодування прот Church кодування:
Pack/Unpack 1 000 000 Inductive Nat Church: {410682,#Fun}
Pack/Unpack 1 000 000 Inductive Nat CPS: {712684,1000000}
Pack/Unpack 1 000 000 Inductive Church List: {717695,'_'}
В два рази повільніше (всього).
data nat : * | (zero: () → nat)
| (succ: nat → nat)
Church
nat () -> [fun (S) -> 1 + S end, 0 ].
zero () -> fun (S) -> fun (Z) -> Z end end.
succ () -> fun (N) -> fun (S)
-> fun (Z) -> S((N(S))(Z)) end end end.
CPS
nat1() -> [fun (F) -> fun (X) -> F(X) + 1 end end, 0 ].
zero1() -> fun (F) -> fun (X) -> X end end.
succ1() -> fun (Z) -> fun (F) -> fun (X)
-> (F(fun(C) -> (C(F))(X) end))(Z) end end end.
ОМ ЛЯМБДА ГАРБХА ХУМ